(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_UFBV)
(declare-fun f0 ( (_ BitVec 113) (_ BitVec 41) (_ BitVec 49)) (_ BitVec 91))
(declare-fun p0 ( (_ BitVec 83) (_ BitVec 117)) Bool)
(declare-fun p1 ( (_ BitVec 42) (_ BitVec 88)) Bool)
(declare-fun v0 () (_ BitVec 33))
(declare-fun v1 () (_ BitVec 46))
(assert (let ((e2(_ bv14053823473644510476726563621 94)))
(let ((e3 (bvnot e2)))
(let ((e4 (ite (p0 ((_ sign_extend 37) v1) ((_ sign_extend 23) e3)) (_ bv1 1) (_ bv0 1))))
(let ((e5 (bvxor e3 ((_ zero_extend 93) e4))))
(let ((e6 (ite (p1 ((_ zero_extend 9) v0) ((_ zero_extend 42) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (bvxor ((_ sign_extend 93) e6) e5)))
(let ((e8 (ite (bvsge e3 e7) (_ bv1 1) (_ bv0 1))))
(let ((e9 (bvsub e2 e5)))
(let ((e10 (ite (p1 ((_ sign_extend 41) e8) ((_ sign_extend 42) v1)) (_ bv1 1) (_ bv0 1))))
(let ((e11 ((_ rotate_right 62) e2)))
(let ((e12 (f0 ((_ sign_extend 67) v1) ((_ extract 58 18) e2) ((_ zero_extend 48) e8))))
(let ((e13 (p0 ((_ sign_extend 82) e10) ((_ sign_extend 71) v1))))
(let ((e14 (p1 ((_ zero_extend 41) e10) ((_ extract 92 5) e7))))
(let ((e15 (bvule e12 ((_ sign_extend 90) e4))))
(let ((e16 (bvsle e3 e2)))
(let ((e17 (bvsgt e3 e9)))
(let ((e18 (p1 ((_ sign_extend 41) e10) ((_ extract 89 2) e11))))
(let ((e19 (p1 ((_ zero_extend 41) e4) ((_ zero_extend 42) v1))))
(let ((e20 (bvugt e9 ((_ zero_extend 3) e12))))
(let ((e21 (bvslt e9 ((_ sign_extend 93) e4))))
(let ((e22 (bvslt ((_ zero_extend 32) e10) v0)))
(let ((e23 (p0 ((_ sign_extend 82) e10) ((_ sign_extend 116) e10))))
(let ((e24 (bvugt ((_ zero_extend 3) e12) e5)))
(let ((e25 (bvsle e12 ((_ zero_extend 45) v1))))
(let ((e26 (= e3 ((_ sign_extend 93) e4))))
(let ((e27 (bvsle e8 e10)))
(let ((e28 (bvsle e4 e6)))
(let ((e29 (ite e24 e23 e14)))
(let ((e30 (= e13 e22)))
(let ((e31 (ite e25 e18 e29)))
(let ((e32 (=> e28 e16)))
(let ((e33 (and e15 e32)))
(let ((e34 (and e27 e19)))
(let ((e35 (or e21 e30)))
(let ((e36 (xor e35 e35)))
(let ((e37 (and e17 e34)))
(let ((e38 (ite e36 e36 e36)))
(let ((e39 (and e20 e26)))
(let ((e40 (not e39)))
(let ((e41 (ite e33 e40 e33)))
(let ((e42 (= e41 e41)))
(let ((e43 (and e31 e37)))
(let ((e44 (not e42)))
(let ((e45 (xor e38 e38)))
(let ((e46 (= e44 e45)))
(let ((e47 (not e43)))
(let ((e48 (=> e46 e47)))
e48
))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
